\begin{tabbing}
$\forall$${\it the\_es}$:ES, $e$:E, $l$:IdLnk, $m$:Msg.
\\[0ex]($m$ $\in$ sends($l$;$e$))
\\[0ex]$\Rightarrow$ \=$\exists$${\it e'}$:rvc($l$,mtag($m$),$v$).($e$ $<$ ${\it e'}$)\+
\\[0ex]\& msgtype($m$) $=$ valtype(${\it e'}$) $\in$ Type \& $v$ $=$ mval($m$) $\in$ valtype(${\it e'}$)
\-
\end{tabbing}